#include <stdio.h>
int A(int x)
{
	D(x);
	B(x);
	printf("A\n");
	return 1;
}

int B(int x)
{
	C(x);
	printf("B\n");
	return 1;
}

int C(int x)
{
	printf("C: there is a bug.\n");
	return 1;
}

int D(int x)
{
	if (x > 0) {
		printf("D: X>0\n");
		A(-x);
	}
	printf("D: X<=0\n");
	return 1;
}

int main(int argc, char **argv)
{
	int x =0;
	klee_make_symbolic(&x, sizeof(x), "xxx");
	printf("main\n");
	A(x);
	return 0;
}
